$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($x$:$A$$\times$$B$($x$)), $C$, $D$:Type, $f$:($C$$\rightarrow$$D$), $b$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$$C$).
\\[0ex]$f$($p$/$x$,$y$. $b$($x$,$y$)) $=$ ($p$/$x$,$y$. $f$($b$($x$,$y$)))